%{
#include <stdio.h>
#include <stdlib.h>
#include <stdarg.h>
#include "lex.yy.h"
#include<iostream>
#include <assert.h>
#include "../../SATSolver/SolverTypes.cuh"
#include "cnf_reader_sintax.cuh"
#include "cnf_reader.cuh"

struct YYSTYPE
{
	int ival;

};

%}

%token <ival> POS_INTEGER
%token <ival> NEG_INTEGER
%token ZERO
%token P
%token CNF

%%


cnf: 
header clauses_list ;

header: 
P CNF POS_INTEGER POS_INTEGER { 
	set_header($3, $4);
	} ;

clauses_list : 
clauses_list clause | clause ;

clause :
{ start_new_clause(); } literals_list ZERO 
	{
	add_clause();
	};

literals_list :
literals_list literal | literal;

literal :
POS_INTEGER { 
	Var v = $1 - 1;
	add_lit(v, true);	
	} | 
	NEG_INTEGER { 
	Var v = (-($1)) - 1;
	add_lit(v, false);
} ;

%%

void yyparse_cnf()
{
	yyparse();
}

